In this paper, we present a formalization of Kozen's propositional modal$\mu$-calculus, in the Calculus of Inductive Constructions. We address severalproblematic issues, such as the use of higher-order abstract syntax ininductive sets in presence of recursive constructors, the encoding of modal(``proof'') rules and of context sensitive grammars. The encoding can be usedin the \Coq system, providing an experimental computer-aided proof environmentfor the interactive development of error-free proofs in the $\mu$-calculus. Thetechniques we adopted can be readily ported to other languages and proofsystems featuring similar problematic issues.
展开▼
机译：在本文中，我们介绍了归纳微积分中Kozen命题模态\ mu $演算的形式化。我们解决了几个问题，例如在递归构造函数存在的情况下使用高阶抽象语法归纳集，模态（``证明''）规则的编码和上下文相关语法的编码。该编码可以在\ Coq系统中使用，为$ \ mu $-演算中的无错误证明的交互式开发提供了实验性的计算机辅助证明环境。我们采用的技术可以很容易地移植到具有类似问题的其他语言和证明系统。
展开▼
